Nuprl Lemma : inr_eq_inl 0,22

AB:Type, x:Ay:B. inr(y) = inl(x A+B  False 
latex


Definitionsx:AB(x), P  Q, False, Prop, t  T

origin